\begin{tabbing}
d{-}world($D$;$v$;${\it sched}$;${\it dec}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$($\lambda$$i$,$x$. M($i$).ds($x$))\+
\\[0ex]$,\,$($\lambda$$i$,$a$. M($i$).da(locl($a$)))
\\[0ex]$,\,$($\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$))
\\[0ex]$,\,$($\lambda$$i$,$t$. \=if $t$=$_{2}$0$\rightarrow$ $\lambda$$x$.M($i$).init($x$)?$v$($i$,$x$)\+
\\[0ex]else 1of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$$-$1,$i$)) fi)
\-\\[0ex]$,\,$($\lambda$$i$,$t$. 1of(2of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$,$i$))))
\\[0ex]$,\,$($\lambda$$i$,$t$. 2of(2of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$,$i$))))
\\[0ex]$,\,$($\lambda$$i$.d{-}machine($i$;M($i$);${\it dec}$($i$)))
\\[0ex]$,\,$$\cdot$$\rangle$
\-
\end{tabbing}